perm filename EXP5.TEX[EKL,SYS] blob
sn#818994 filedate 1986-06-13 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00006 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 % ekl macros
C00008 00003 \catcode`\_=12 % we always use ↓ for subscripts
C00015 00004 % perm macros
C00016 00005 % Title page
C00018 00006 The following lines are labeled /simpinfo/ in some proof. They are available to
C00040 ENDMK
C⊗;
% ekl macros
%\magnification = \magstep1 % Entire document is magnified
\magnification = \magstephalf % Entire document is magnified
\newwrite\contentsfile
\newwrite\findexfile
\openout\contentsfile = perm.toc
\openout\findexfile = findex.raw
\raggedbottom
% Font definitions:
\font\tt = cmtex10 % typewriter type (TeX character set)
\font\tencsc = cmcsc10 % for page headings
\font\titlefont = cmbx10 at 12truept % for title page
\font\stanford = stan70 at 70truept % Stanford seal
\font\eighttt = cmtex8 % typewriter type (TeX character set)
% \font\ninerm=amr9
% \font\eightrm=amr8
% \font\sixrm=amr6
% \font\ninei=ammi9
% \font\eighti=ammi8
% \font\sixi=ammi6
% \skewchar\ninei='177
% \skewchar\eighti='177
% \skewchar\sixi='177
% \font\ninesy=amsy9
% \font\eightsy=amsy8
% \font\sixsy=amsy6
% \font\nineit=amti9
% \font\eightit=amti8
% \font\sevenit=amti7
% \font\ninebf=ambx9
% \font\eightbf=ambx8
% \font\sixbf=ambx6
% \font\ninett=amtt9
% \font\eighttt=amtt8
% \hyphenchar\tentt=-1 % inhibit hyphenation in typewriter type
% \hyphenchar\ninett=-1
% \hyphenchar\eighttt=-1
% \newskip\ttglue
% \def\tenpoint{\def\rm{\fam0\tenrm}%
% \textfont0=\tenrm \scriptfont0=\sevenrm \scriptscriptfont0=\fiverm
% \textfont1=\teni \scriptfont1=\seveni \scriptscriptfont1=\fivei
% \textfont2=\tensy \scriptfont2=\sevensy \scriptscriptfont2=\fivesy
% \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex
%
% \def\it{\fam\itfam\tenit}%
% \textfont\itfam=\tenit \scriptfont\itfam=\sevenit
%
% \def\bf{\fam\bffam\tenbf}%
% \textfont\bffam=\tenbf \scriptfont\bffam=\sevenbf
%
% \def\tt{\fam\ttfam\tentt}%
% \textfont\ttfam=\tentt \scriptfont\ttfam=\eighttt
% \tt \ttglue=.5em plus.25em minus.15em
%
% \normalbaselineskip=12pt
% \setbox\strutbox=\hbox{\vrule height8.5pt depth3.5pt width\z@}%
% \normalbaselines\rm
% }
% \def\ninepoint{\def\rm{\fam0\ninerm}%
% \textfont0=\ninerm \scriptfont0=\sixrm \scriptscriptfont0=\fiverm
% \textfont1=\ninei \scriptfont1=\sixi \scriptscriptfont1=\fivei
% \textfont2=\ninesy \scriptfont2=\sixsy \scriptscriptfont2=\fivesy
% \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex
% \def\it{\fam\itfam\nineit}%
% \textfont\itfam=\nineit \scriptfont\itfam=\sixi
% \def\bf{\fam\bffam\ninebf}%
% \textfont\bffam=\ninebf \scriptfont\bffam=\sixbf
% \def\tt{\fam\ttfam\ninett}%
% \textfont\ttfam=\ninett
% \tt \ttglue=.5em plus.25em minus.15em
% \normalbaselineskip=10.5pt
% \setbox\strutbox=\hbox{\vrule height8pt depth3pt width\z@}%
% \normalbaselines\rm
% }
% \def\eightpoint{\def\rm{\fam0\eightrm}%
% \textfont0=\eightrm \scriptfont0=\sixrm \scriptscriptfont0=\fiverm
% \textfont1=\eighti \scriptfont1=\sixi \scriptscriptfont1=\fivei
% \textfont2=\eightsy \scriptfont2=\sixsy \scriptscriptfont2=\fivesy
% \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex
% \def\it{\fam\itfam\eightit}%
% \textfont\itfam=\eightit \scriptfont\itfam=\sixi
% \def\bf{\fam\bffam\eightbf}%
% \textfont\bffam=\eightbf \scriptfont\bffam=\sixbf
% \def\tt{\fam\ttfam\eighttt}%
% \textfont\ttfam=\eighttt
% \tt \ttglue=.5em plus.25em minus.15em
% \normalbaselineskip=9pt
% \setbox\strutbox=\hbox{\vrule height7pt depth2pt width\z@}%
% \normalbaselines\rm
% }
\catcode`\_=12 % we always use ↓ for subscripts
% Often, we want to put text in the typewriter font. In simple cases, we use
% the form /FOO/. If it has special characters or multiple blanks, we say
% \\/FOOBAR/\\ which allows arbitrary stuff (except the / or \ characters) in
% FOOBAR, but takes more TeX processing time.
\catcode`/=13 \def/#1/{\hbox{\tt\frenchspacing#1}}
% When there are just a few characters requiring special treatment, we can use
% the predefined macros \#, \&, and \%, or the following:
\def\↑{\char11 }
\def\↓{\char1 }
\def\uncatcode{\catcode`\{=12 % undoes most of TeX's character codes
\catcode`\}=12
\catcode`\$=12
\catcode`\&=12
\catcode`\%=12
\catcode`\#=12
\catcode`\↑=12
\catcode`\↓=12
\catcode`\ =12}
\def\\{\begingroup \let\\=\endgroup \uncatcode}
% The following are commonly used macros:
\def\.{\spacefactor1000 . } % use for end of sentence after a capital letter
\def\xskip{\hskip7pt plus3pt minus4pt}
% The following macros set things up so that we can write lines of terminal
% interaction in the form
%
% \lines
% ...
% \endlines
%
% The \slines macro is similar, except it spaces its lines more closely together.
{\catcode`\↑↑M=13\global\let ↑↑M=\break} % This must be on one line!
\def\lines{\par\begingroup
\def\eat##1{}
\uncatcode
\parindent 0pt
\leftskip 25pt
\rightskip 0pt plus 1fil
\interlinepenalty 50
\baselineskip 12pt
\parskip 12pt plus 6pt minus 6pt
\catcode`\↑↑M=13
\tt\eat}
\def\slines{\par\begingroup
\def\eat##1{}
\uncatcode
\parindent 0pt
\leftskip 25pt
\rightskip 0pt plus 1fil
\interlinepenalty 50
\baselineskip 10.5pt
\parskip 10pt plus 5pt minus 5pt
\catcode`\↑↑M=13
\tt\eat}
\def\nlines{\par\begingroup
\def\eat##1{}
\uncatcode
\parindent 0pt
\leftskip 25pt
\rightskip 0pt plus 1fil
\interlinepenalty 50
\baselineskip 8.5pt
\parskip 8pt plus 4pt minus 4pt
\catcode`\↑↑M=13
\eighttt\eat}
\def\endlines{\par\vskip-\baselineskip % cancel the last empty line
\vskip\the\parskip % put in space
\endgroup\vskip-\parskip} % cancel the next space to go in
\let\eat=\relax % outside \lines, for indexing to work
% Formula index. \eat prevents extra blank line if used inside \lines.
\def\fx∂#1∂#2∂{\write\findexfile{∂#1!\the\count0!#2!}\eat}
% The following macros implement a rather hairy section numbering scheme.
% The purpose is to allow both forward and backward section references,
% without pre-knowledge of the section numbers, so that sections can be
% inserted or moved easily.
% All sections are represented by TeX macros. On the next page, we will copy
% the lines from the directory page of this file that define the beginning of
% each section. Each section must, therefore, begin on a new page. First we
% define the \section, \subsection, and \subsubsection macros that will be
% used at the beginning of each section in the text, and the macros for section
% references.
\outer\def\section#1#2{\vfill\eject\message{#2}
\mark{Section #1}
\write\contentsfile{∂#1. #2. \the\count0.}
\hbox{\bf\relax #1.\hskip 1em #2.}
\vskip 20pt plus 20pt minus 5pt}
\outer\def\subsection#1#2{\penalty-100\vskip 20pt plus 20pt minus 5pt
\write\contentsfile{∞#1. #2. \the\count0.}
\hbox{\bf\relax #1.\hskip 1em #2.}
\penalty10000\vskip 15pt plus 15pt minus 5pt}
\let\subsubsection=\subsection
\def\sectionref#1{section\penalty9999\ #1} % lowercase version
\def\Sectionref#1{Section\penalty9999\ #1} % uppercase version
\nopagenumbers % supress footlines
\def\title{About Permutations in Lisp and EKL}
\headline={\ifodd\pageno \hfil{\tencsc\firstmark}\hfil{\tenrm \folio}
\else {\tenrm\folio}\hfil{\tencsc\title}\hfil \fi}
\voffset=2\baselineskip % as the TeXbook recommends
\vsize=8.6truein % else we don't get 1-inch bottom margin
\hsize=6.5truein
% perm macros
\def\inmmode#1{\relax\ifmmode #1\else $#1$\fi}
\def\NUM{{\bf N}}
\def\num#1{\inmmode{{\bf N}↓{#1}}} % initial segment of N
% \num1
% \num{n}
\def\cpile#1{\vcenter{\halign{\hfil$## $\hfil\crcr#1}}}
\def\qdot{\inmmode{\mathrel{\raise .3ex\hbox{$\scriptscriptstyle{\bullet}$}}}}
% \def\⊗{\mathbin{\raise .2ex\hbox{$\scriptstyle{\otimes}$}}}
\def\⊗{\circ}
\def\bull{\vrule height 1.3ex width 1.0ex depth -.1ex }
% Title page
{\output{} % \output is local to this page
\topskip 1.5truein
{\baselineskip 15pt \bf
\centerline{\titlefont Experiments in Automatic Theorem Proving}
\centerline{by}
\centerline{Gian Luigi Bellin and Jussi Ketonen}} % end \bf
\vfill
\centerline{Research Sponsored by}
\vskip 6pt
\centerline{Advanced Research Projects Agency}
\centerline{and}
\centerline{National Science Foundation}
\vfill
\centerline{\bf Department of Computer Science}
\centerline{Stanford University}
\centerline{Stanford, CA 94305}
\vskip 18pt
\centerline{\stanford S}
\vfill
\centerline{This version of the PERM was printed on
\ifcase\the\month \or January\or February\or March\or April\or May\or June\or
July\or August\or September\or October\or November\or December\fi
\ \the\day, \the\year.}
\eject}
The following lines are labeled /simpinfo/ in some proof. They are available to
/EKL/ in the execution of all proofs that use the proof in question by the
command /get-proofs/ (see the graph of file dependency at the beginning of the
Appendix).
\bigskip
{\bf from file LISPAX}
\smallskip
{\bf proof LISPAX}
\slines
13. ∀XA.SEXP XA
\endlines
\slines
14. ∀U.SEXP U
\endlines
\slines
15. ∀X U.LISTP X.U
\endlines
\slines
16. ∀U.¬NULL U⊃LISTP CDR U
\endlines
\slines
17. ∀U.¬NULL U⊃SEXP CAR U
\endlines
\slines
18. ∀X.¬ATOM X⊃SEXP CAR X
\endlines
\slines
19. ∀X.¬ATOM X⊃SEXP CDR X
\endlines
\slines
20. ∀X Y.SEXP X.Y
\endlines
\slines
21. ∀X Y.¬ATOM X.Y
\endlines
\slines
22. ∀X U.¬NULL X.U
\endlines
\slines
23. ∀U.NULL U⊃U=NIL
\endlines
\slines
24. ∀X Y.CAR (X.Y)=X
\endlines
\slines
25. ∀X Y.CDR (X.Y)=Y
\endlines
\slines
26. CAR NIL=NIL
\endlines
\slines
27. CDR NIL=NIL
\endlines
\slines
28. ∀U.¬NULL U⊃CAR U.CDR U=U
\endlines
\slines
;labels: SIMPINFO CONS_CAR_CDR
29. ∀X.¬ATOM X⊃CAR X.CDR X=X
\endlines
\slines
43. LIST(())=NIL
\endlines
\slines
44. ∀LST.LISTP LIST(LST)
\endlines
\slines
;labels: SIMPINFO LISTDEF
45. ∀X LST.LIST(X,LST)=X.LIST(LST)
\endlines
\slines
;labels: SIMPINFO APPENDEF
47. ∀X U V.NIL*V=V∧X.U*V=X.(U*V)
\endlines
\slines
;labels: SIMPINFO LISTAPPEND
48. ∀U V.LISTP U*V
\endlines
\slines
49. ∀U.U*NIL=U
\endlines
\slines
50. ∀X V.X.NIL*V=X.V
\endlines
\slines
56. ∀ALIST.LISTP ALIST
\endlines
\slines
58. ALISTP NIL
\endlines
\slines
;labels: SIMPINFO MKALIST
59. ∀XA Y ALIST.ALISTP (XA.Y).ALIST
\endlines
\slines
62. ∀X ALIST.SEXP ASSOC(X,ALIST)
\endlines
\slines
67. ∀U.SEXP CAR U
\endlines
\slines
68. ∀U.LISTP CDR U
\endlines
\vfill\eject
{\bf from file NATNUM}
\smallskip
{\bf proof NATNUM}
\slines
10. ∀N.NATNUM(N')
\endlines
\slines
;labels: SIMPINFO PRED_DEF
19. ∀N.PRED(N')=N
\endlines
\slines
20. ∀N.NATNUM(PRED(N))
\endlines
\slines
;labels: SIMPINFO PLUSFACTS PLUSDEF
21. ∀N K.0+N=N∧K'+N=(K+N)'
\endlines
\slines
22. ∀N M.NATNUM(N+M)
\endlines
\slines
;labels: SIMPINFO PLUSFACTS
23. ∀N.N+0=N
\endlines
\slines
;labels: SIMPINFO PLUSFACTS PLUSDEF1
24. ∀N.1+N=N'∧N+1=N'
\endlines
\slines
;labels: SIMPINFO PLUSFACTS
25. ∀N K.N+K'=(N+K)'
\endlines
\slines
;labels: SIMPINFO SUCCFACTS ZERO_NOT_SUCCESSOR
17. ∀N.¬N'=0
\endlines
\slines
;labels: SIMPINFO ZEROLEAST1
9. ∀N.¬N<0
\endlines
\slines
;labels: SIMPINFO SUCCFACTS SUCCESSORLESS
13. ∀N M.N'<M'≡N<M
\endlines
\slines
;labels: SIMPINFO SUCCFACTS SUCCESSOREQ
14. ∀N M.N'=M'≡N=M
\endlines
\slines
;labels: SIMPINFO SUCCFACTS ZEROLEAST3
16. ∀N.0<N'
\endlines
\vfill\eject
{\bf from file MINUS}
\smallskip
{\bf proof LESSEQ}
\slines
1. ∀N.¬N=N'
\endlines
\slines
;labels: SIMPINFO SUCCESSORFACTS SUCCESSORLESSEQ
4. ∀N M.N'≤M'≡N≤M
\endlines
\slines
;labels: SIMPINFO ZERO_NON_LESS_SUCCESSOR
9. ∀N M.N'<M⊃¬M=0
\endlines
\smallskip
{\bf proof MINUS}
\slines
;labels: SIMPINFO MINUS_SORT
3. ∀N K.NATNUM(K-N)
\endlines
\slines
;labels: SIMPINFO N_LESS_N
9. ∀N.N-N=0
\endlines
\bigskip
{\bf from file LENGTH}
\smallskip
{\bf proof LENGTH}
\slines
;labels: SIMPINFO LENGTHDEF
2. ∀U X.LENGTH NIL=0∧LENGTH (X.U)=LENGTH U'
\endlines
\slines
3. ∀U.NATNUM(LENGTH U)
\endlines
\slines
4. ∀U.LENGTH U=0≡NULL U
\endlines
\slines
;labels: SIMPINFO LENGTHADD
5. ∀U V.LENGTH (U*V)=LENGTH U+LENGTH V
\endlines
\slines
6. ∀X.LENGTH (X.NIL)=1
\endlines
\slines
;labels: SIMPINFO HAVE_MEMBER
8. ∀U Y.MEMBER(Y,U)⊃0<LENGTH U
\endlines
\slines
;labels: SIMPINFO HAVE_MEMBER1
9. ∀U Y.MEMBER(Y,U)⊃¬NULL U
\endlines
\vfill\eject
{\bf from file NTH}
\smallskip
{\bf proof LISPAX}
\slines
69. ∀N.¬NULL N
\endlines
\slines
70. ∀N.SEXP N
\endlines
\smallskip
{\bf proof NTH}
\slines
;labels: SIMPINFO NTHDEF
2. ∀X U N.NTH(NIL,N)=NIL∧NTH(U,0)=CAR U∧NTH(X.U,N')=NTH(U,N)
\endlines
\slines
;labels: SIMPINFO SEXP_NTH
3. ∀U N.SEXP NTH(U,N)
\endlines
\smallskip
{\bf proof NTH}
\slines
;labels: SIMPINFO NTHCDRDEF
2. ∀X U N.NTHCDR(NIL,N)=NIL∧NTHCDR(U,0)=U∧NTHCDR(X.U,N')=NTHCDR(U,N)
\endlines
\slines
3. ∀U N.LISTP NTHCDR(U,N)
\endlines
\smallskip
{\bf proof FSTPOSITION}
\slines
;labels: SIMPINFO POSFACTS
3. ∀U Y.(NULL FSTPOSITION(U,Y)⊃¬MEMBER(Y,U))∧
(MEMBER(Y,U)⊃NATNUM(FSTPOSITION(U,Y)))∧
(NULL FSTPOSITION(U,Y)∨NATNUM(FSTPOSITION(U,Y)))
\endlines
\slines
;labels: SIMPINFO SORTPOS
4. ∀U Y.SEXP FSTPOSITION(U,Y)
\endlines
\vfill\eject
{\bf from file APPL}
\smallskip
{\bf proof ALISTFACTS}
\slines
;labels: SIMPINFO DOMSORT
1. ∀ALIST.LISTP DOM(ALIST)
\endlines
\slines
;labels: SIMPINFO RANGESORT
2. ∀ALIST.LISTP RANGE(ALIST)
\endlines
\slines
;labels: SIMPINFO APPALISTSORT
5. ∀ALIST Y.SEXP APPALIST(Y,ALIST)
\endlines
\smallskip
{\bf proof APPL}
\slines
;labels: SIMPINFO APPLFACTS
3. ∀U I.I<LENGTH U⊃SEXP APPL(U,I)∧MEMBER(APPL(U,I),U)
\endlines
\slines
;labels: SIMPINFO NUMSEQ_TOTAL
4. ∀K NUMSEQ.NATNUM(NUMSEQ(K))
\endlines
\smallskip
{\bf from file SUMS}
\smallskip
{\bf proof SUMFACTS}
\slines
;labels: SIMPINFO SUMSORT
5. ∀K NUMSEQ.NATNUM(SUM(NUMSEQ,K))
\endlines
\bigskip
{\bf from file MULT}
\smallskip
{\bf proof MULTIPLICITY}
\slines
;labels: SIMPINFO MULTFACT
3. ∀U A.NATNUM(MULT(U,A))
\endlines
\slines
;labels: SIMPINFO EMPTYFACTS
7. ∀U.MULT(U,EMPTYSET)=0
\endlines
\bigskip
{\bf from file ASSOC}
\smallskip
{\bf proof ALISTFACTS}
\slines
;labels: SIMPINFO COMPALISTSORT
11. ∀ALIST ALIST1.ALISTP ALIST∞ALIST1
\endlines
\vfill\eject
{\bf from file PERMF}
\smallskip
{\bf proof PERMFACTS}
\slines
;labels: SIMPINFO SORTCOMP
2. ∀V U.DEF_APPL(V,U)⊃LISTP V⊗U
\endlines
\slines
3. ∀V U.ALLP(λX.NATNUM(X)∧X<LENGTH V,U)⊃LISTP V⊗U
\endlines
\slines
4. ∀M N.LISTP IDENT1(M,N)
\endlines
\slines
5. ∀N.LISTP IDENT(N)
\endlines
\slines
6. ∀U N I.LISTP INVERS1(U,I,N)
\endlines
\slines
7. ∀U.LISTP INVERSE(U)
\endlines
\slines
;labels: SIMPINFO IDENT_LENGTH
9. ∀N M.LENGTH (IDENT1(M,N))=N
\endlines
\slines
10. ∀N.LENGTH (IDENT(N))=N
\endlines
\end